Double negation

 ( Theorems In Propositional Logic ) 

In propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionistic logic; this can be expressed by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign expresses negation.

Like the law of the excluded middle, this principle is considered to be a law of thought in classical logic,Hamilton is discussing Hegel in the following: "In the more recent systems of philosophy, the universality and necessity of the axiom of Reason has, with other logical laws, been controverted and rejected by speculators on the absolute. On" (Hamilton 1860:68) but it is disallowed by intuitionistic logic.The ^o of Kleene's formula *49^o indicates "the demonstration is not valid for both systems classical", Kleene 1952:101. The principle was stated as a theorem of propositional logic by Bertrand Russell and Whitehead in Principia Mathematica'' as:

: $\backslash mathbf\{*4\backslash cdot13\}.\; \backslash \; \backslash \; \backslash vdash.\backslash \; p\; \backslash \; \backslash equiv\; \backslash \; \backslash thicksim(\backslash thicksim\; p)$PM 1952 reprint of 2nd edition 1927 pp. 101–02, 117.

:"This is the principle of double negation, i.e. a proposition is equivalent of the falsehood of its negation."

---

Elimination and introduction Double negation elimination and double negation introduction are two valid rules of replacement. They are the that, if not not-A is true, then A is true, and its converse, that, if A is true, then not not-A is true, respectively. The rule allows one to introduce or eliminate a negation from a formal proof. The rule is based on the equivalence of, for example, It is false that it is not raining. and It is raining.

The double negation introduction rule is:

P $\backslash Rightarrow$ P

and the double negation elimination rule is:

P $\backslash Rightarrow$ P

Where "$\backslash Rightarrow$" is a symbol representing "can be replaced in a proof with."

In logics that have both rules, negation is an involution.

---

Formal notation The double negation introduction rule may be written in sequent notation:

$P\; \backslash vdash\; \backslash neg\; \backslash neg\; P$

The double negation elimination rule may be written as:

$\backslash neg\; \backslash neg\; P\; \backslash vdash\; P$

In inference rule:

$\backslash frac\{P\}\{\backslash neg\; \backslash neg\; P\}$

and

$\backslash frac\{\backslash neg\; \backslash neg\; P\}\{P\}$

or as a tautology (plain propositional calculus sentence):

$P\; \backslash to\; \backslash neg\; \backslash neg\; P$

and

$\backslash neg\; \backslash neg\; P\; \backslash to\; P$

These can be combined into a single biconditional formula:

$\backslash neg\; \backslash neg\; P\; \backslash leftrightarrow\; P$.

Since biconditionality is an equivalence relation, any instance of ¬¬ A in a well-formed formula can be replaced by A, leaving unchanged the truth-value of the well-formed formula.

Double negative elimination is a theorem of classical logic, but not of weaker logics such as intuitionistic logic and minimal logic. Double negation introduction is a theorem of both intuitionistic logic and minimal logic, as is $\backslash neg\; \backslash neg\; \backslash neg\; A\; \backslash vdash\; \backslash neg\; A$.

Because of their constructive character, a statement such as It's not the case that it's not raining is weaker than It's raining. The latter requires a proof of rain, whereas the former merely requires a proof that rain would not be contradictory. This distinction also arises in natural language in the form of litotes.

---

Proofs

---

In classical propositional calculus system In Hilbert system for propositional logic, double negation is not always taken as an axiom (see list of Hilbert systems), and is rather a theorem. We describe a proof of this theorem in the system of three axioms proposed by Jan Łukasiewicz:

A1. $\backslash phi\; \backslash to\; \backslash left(\; \backslash psi\; \backslash to\; \backslash phi\; \backslash right)$

A2. $\backslash left(\; \backslash phi\; \backslash to\; \backslash left(\; \backslash psi\; \backslash rightarrow\; \backslash xi\; \backslash right)\; \backslash right)\; \backslash to\; \backslash left(\; \backslash left(\; \backslash phi\; \backslash to\; \backslash psi\; \backslash right)\; \backslash to\; \backslash left(\; \backslash phi\; \backslash to\; \backslash xi\; \backslash right)\; \backslash right)$

A3. $\backslash left\; (\; \backslash lnot\; \backslash phi\; \backslash to\; \backslash lnot\; \backslash psi\; \backslash right)\; \backslash to\; \backslash left(\; \backslash psi\; \backslash to\; \backslash phi\; \backslash right)$

We use the lemma $p\; \backslash to\; p$ proved here, which we refer to as (L1), and use the following additional lemma, proved here:

(L2) $p\; \backslash to\; ((p\; \backslash to\; q)\; \backslash to\; q)$

We first prove $\backslash neg\; \backslash neg\; p\; \backslash to\; p$. For shortness, we denote $q\; \backslash to\; (\; r\; \backslash to\; q\; )$ by φ₀. We also use repeatedly the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

(1) $\backslash varphi\_0$       (instance of (A1))

(2) $(\backslash neg\; \backslash neg\; \backslash varphi\_0\; \backslash to\; \backslash neg\; \backslash neg\; p\; )\; \backslash to\; (\backslash neg\; p\; \backslash to\; \backslash neg\; \backslash varphi\_0)$       (instance of (A3))

(3) $(\backslash neg\; p\; \backslash to\; \backslash neg\; \backslash varphi\_0)\; \backslash to\; (\backslash varphi\_0\; \backslash to\; p\; )$       (instance of (A3))

(4) $(\backslash neg\; \backslash neg\; \backslash varphi\_0\; \backslash to\; \backslash neg\; \backslash neg\; p\; )\; \backslash to\; (\backslash varphi\_0\; \backslash to\; p\; )$       (from (2) and (3) by the hypothetical syllogism metatheorem)

(5) $\backslash neg\; \backslash neg\; p\; \backslash to\; (\; \backslash neg\; \backslash neg\; \backslash varphi\_0\; \backslash to\; \backslash neg\; \backslash neg\; p\; )$       (instance of (A1))

(6) $\backslash neg\; \backslash neg\; p\; \backslash to\; (\backslash varphi\_0\; \backslash to\; p\; )$       (from (4) and (5) by the hypothetical syllogism metatheorem)

(7) $\backslash varphi\_0\; \backslash to\; ((\backslash varphi\_0\; \backslash to\; p)\; \backslash to\; p)$       (instance of (L2))

(8) $(\backslash varphi\_0\; \backslash to\; p)\; \backslash to\; p$       (from (1) and (7) by modus ponens)

(9) $\backslash neg\; \backslash neg\; p\; \backslash to\; p$       (from (6) and (8) by the hypothetical syllogism metatheorem)

We now prove $p\; \backslash to\; \backslash neg\; \backslash neg\; p$.

(1) $\backslash neg\backslash neg\backslash neg\; p\; \backslash to\; \backslash neg\; p$       (instance of the first part of the theorem we have just proven)

(2) $(\backslash neg\backslash neg\backslash neg\; p\; \backslash to\; \backslash neg\; p)\; \backslash to\; (p\; \backslash to\; \backslash neg\backslash neg\; p)$       (instance of (A3))

(3) $p\; \backslash to\; \backslash neg\; \backslash neg\; p$       (from (1) and (2) by modus ponens)

And the proof is complete.

---

See also

• Gödel–Gentzen negative translation

---

Bibliography

• William Hamilton, 1860, Lectures on Metaphysics and Logic, Vol. II. Logic; Edited by Henry Mansel and John Veitch, Boston, Gould and Lincoln.
• Christoph Sigwart, 1895, Logic: The Judgment, Concept, and Inference; Second Edition, Translated by Helen Dendy, Macmillan & Co. New York.
• Stephen C. Kleene, 1952, Introduction to Metamathematics, 6th reprinting with corrections 1971, North-Holland Publishing Company, Amsterdam NY, .
• Stephen C. Kleene, 1967, Mathematical Logic, Dover edition 2002, Dover Publications, Inc, Mineola N.Y.
• Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, 2nd edition 1927, reprint 1962, Cambridge at the University Press.

Post Comment